.NH
Conclusions and Future Work
.PP
We have shown specification techniques for hardware behavior
using the logic programming language, Tokio, which is based on LTTL
with interval signals.
Using Tokio, behaviors of various levels, from algorithm to gates,
are easily described.
We also presented an interpreter for Tokio and several example runs.
Using the interpreter, designers can check their Tokio programs.
.PP
The details of the compiler will be reported elsewhere.
.PP
The formal verification and synthesis of Tokio programs are
future research topics.
We are now describing various real hardwares in Tokio.
This provides a lot of
experience and indicates important points.
We think by including theorem proving techniques for first order logic,
our verification and synthesis techniques can be applied to
Tokio programs.
